$\forall$$A$,$B$:es\_realizer\{i:l\}.
\\[0ex]R{-}compat\{i:l\}($A$; $B$) $\Rightarrow$ ($\forall$$i$:Id. fpf{-}compatible(Id; $x$.Type; id{-}deq; R{-}ds($A$; $i$); R{-}ds($B$; $i$)))